Abstract: Among other uses, the turnstile sign is utilized by logicians for denoting a consequence relation, related to a given logic, between collections of formulas and formulas. This package aims to issue the turnstile sign in many ways, and is capable of putting labels below and above it. This paper is a brief tutorial and gives many examples.
Abstract: A nonmonotonic logic, the Logic of Plausible Reasoning – LPR – capable of coping with the demands of what we call "complex reasoning", is introduced. It is argued that creative complex reasoning is the way of reasoning required in many instances of scientific thought, professional practice and common life decision taking. For managing the simultaneous consideration of multiple scenarios inherent in these activities, two new modalities, weak and strong plausibility, are introduced as part of the Logic of Plausible Deduction – LPD – a deductive logic specially designed to serve as the monotonic support for LPR. Axiomatics and semantics for LPD, together with a completeness proof, are provided. Once LPD has been given, LPR may be defined via a concept of extension over LPD. Although the construction of LPR extensions is first presented in standard style, for the sake of comparison with existing nonmonotonic formalisms like Reiter’s one, alternative more elegant and intuitive ways for constructing nonmonotonic LPR extensions are also given and proofs of their equivalence are presented.
Abstract: This article presents an alternative form of generating tree proofs
by tableaux, which is denominated direct, due to the characteristic in which
the possible conclusion is inserted in the initial tableau, without denying
it. The tableau method by refutation uses instead the denial of the possible
conclusion. In the tableau system by direct proof for classical logic, each
branch corresponds semantically to the disjunction of all formulas that
compose it, and any tableau is semantically equivalent to the conjunction
of all these disjunctions. For each one of the tableau based methods for
classical logic, the direct or the indirect one, a branch is considered
closed if the same contains two contradictory formulas. In the direct method
the closure of a branch corresponds to its validity, which implies, in case
of closure of all branches, to the validity of the possible conclusion,
whereas in the indirect method the closure of all branches entails the unsatisfiability
of the denial of the possible conclusion, which in its turn implies its
validity.
Introduction of Implication
and Generalization in Axiomatic Calculi, by Arthur Buchsbaum and Jean-Yves Béziau
Travaux de Logique, v. 17, Aspects of Universal Logic,
edited by Jean-Yves Béziau, Alexandre Costa Leite and Alessandro
Facchini, Centre de Recherches Sémiologiques,
Université de Neuchâtel, pgs. 231-254, 2004.
Abstract: Aiming clear formulations of deduction theorem
and some possible restrictions to their application, it is done a study
concerning to rules of introduction of implication and of generalization,
taking into account their connection with varying objects, which generalize
the idea of variables. Some concepts and techniques concerning to their
tracing are introduced. A classification of axiomatic calculi with respect
to their relationship with deduction theorem is done.
Abstract: A logic formalizing ambiguity, which is present both in natural
language as in mathematical discourse, is presented, through a sequent calculus
and a semantics, together with some elementary results.
A General Treatment for the Deduction Theorem
in Open Calculi, by Arthur Buchsbaum and Tarcisio Pequeno
Logique et Analyse, v. 157, no II, pp. 9-29,
1997.
Abstract: The rules of introduction of implication and of generalization
are closely connected, and can be described by varying objects, which trace
how generalization rules are used inside a demonstration. Some forms on
introduction of implication and of generalization are presented, taking
into account basic properties that axiomatic calculi can have.
A Reasoning Method for
a Paraconsistent Logic, by Arthur Buchsbaum and Tarcisio Pequeno
Studia Lógica, v. 52, no 2, pp. 281-289,
1993. Varsóvia, Polônia.
Abstract: A method of automated proof for a paraconsistent logic, the C1*
calculus of Newton C. A. da Costa, is presented. It is analytic, and is
based on tableaux. Actually, two tableau systems were defined: one with
a small number of rules, from which it is proved the correctness and completeness
of the method, and other one, which is equivalent to the former, is a system
of derived rules, from which was done an implementation.
O Método dos Tableaux Generalizado e sua
Aplicação ao Raciocínio Automático em Lógicas Não Clássicas, by Arthur Buchsbaum and Tarcisio Pequeno
Série "O que nos faz pensar", Cadernos do Departamento
de Filosofia da PUC-Rio, Rio de Janeiro, v. 3, pp. 81-96, 1990.
Abstract: A presentation of tableau method in a way which
does not depend from any specific logic, including examples for classical
quantificational logic and the paracomplete logic P1
of Newton C. A. da Costa, together with some heuristics for construction
of tableau systems.
Resumo: Entre outros usos, a barra de Frege é utilizada pelos lógicos para denotar a relação de conseqüência, com respeito a uma dada lógica, entre coleções de fórmulas e fórmulas. O pacote turnstile foi feito para desenhar a barra de Frege em várias formas, e para colocar dados abaixo e acima deste símbolo. Este artigo é um breve tutorial e dá vários exemplos.
Resumo: Uma lógica não monotônica, a Lógica do Raciocínio Plausível – LPR – capaz de lidar com as demandas do que chamamos de "raciocínio complexo", é apresentada. É argumentado que o raciocínio complexo criativo é o estilo de raciocínio requerido em muitas formas do pensamento científico, da prática profissional, e na tomada de decisões da vida comum. Para gerenciar a consideração simultânea de múltiplos cenários inerente a estas atividades, duas novas modalidades, a plausibilidade fraca e a forte, são introduzidas, como integrantes da Lógica da Dedução Plausível – LPD – uma lógica dedutiva especialmente concebida como suporte monotônico para LPR. Uma axiomática e uma semântica para LPD, juntamente com uma prova de completude para LPD, são dadas. LPR pode ser definido através de um conceito de extensão por LPD. Embora as extensões em LPR sejam apresentadas primeiramente no estilo padrão de Raymond Reiter, à guisa de comparação com formalismos não monotônicos já existentes, formas alternativas mais elegantes e intuitivas para a construção de extensões em LPR são também dadas, bem como provas de sua equivalência com extensões em LPR.
Resumo: Uma forma alternativa de geração de árvores de provas por tablôs
é apresentada. Denominamos esse método de direto, por causa de característica
em que a possível conclusão é inserida no tablô inicial, sem negá-la. No
sistema de tablôs por prova direta para a lógica clássica, cada ramo corresponde
semanticamente à disjunção das fórmulas que o compõem, e cada tablô equivale
semanticamente à conjunção de todas essas disjunções. Neste método o fechamento
de um ramo acarreta a sua validade semântica, a qual por sua vez implica,
no caso do fechamento de todos os ramos, na validade da possível conclusão.
Introduction of Implication
and Generalization in Axiomatic Calculi, de Arthur Buchsbaum e Jean-Yves Béziau
Travaux de Logique, v. 17, Aspects of Universal Logic,
editado por Jean-Yves Béziau, Alexandre Costa Leite e Alessandro
Facchini, Centre de Recherches Sémiologiques,
Université de Neuchâtel, pgs. 231-254, 2004.
Resumo: Visando formulações claras do
teorema da dedução e de possíveis restrições
à sua aplicação, um estudo concernente às regras
de introdução da implicação e da generalização
é realizado, levando em conta a sua conexão com objetos variantes,
os quais generalizam a idéia de variáveis. Alguns conceitos
e técnicas concernentes ao seu rastreamento são introduzidos.
Como resultado, uma classificação dos cálculos com
respeito ao seu relacionamento com o teorema da dedução é
feita.
Resumo: Uma lógica que formaliza a ambigüidade, a qual está presente tanto
na linguagem natural como no discurso matemático, é apresentada, através
de um cálculo de seqüentes e de uma semântica, juntamente com alguns resultados
elementares.
A General Treatment for the Deduction Theorem
in Open Calculi, de Arthur Buchsbaum e Tarcisio Pequeno
Logique et Analyse, v. 157, nº II, pgs. 9-29,
1997.
Resumo: As regras de introdução da implicação e da generalização estão intimamente
relacionadas, e podem ser descritas por objetos variantes, os quais rastreiam
como as regras da generalização são usadas em uma demonstração. Algumas
formas da introdução da implicação e da generalização são apresentadas,
levando em conta propriedades básicas que os cálculos axiomáticos podem
possuir.
A Reasoning Method for
a Paraconsistent Logic, de Arthur Buchsbaum e Tarcisio Pequeno
Studia Lógica, v. 52, nº 2, pgs. 281-289,
1993. Varsóvia, Polônia.
Resumo: Um método de prova automático para uma lógica paraconsistente, o
cálculo C1* de Newton C. A. da Costa, é apresentado.
Trata-se de um método analítico utilizando um sistema de tableaux. Na realidade,
dois sistemas de tableaux foram elaborados: um com um número pequeno de
regras, a partir do qual são provadas a consistência e a completude do método,
e outro, que mostramos ser equivalente ao primeiro, é um sistema de regras
derivadas, a partir do qual foi realizada uma implementação.
O Método dos Tableaux Generalizado e sua
Aplicação ao Raciocínio Automático em Lógicas Não Clássicas, de Arthur Buchsbaum e Tarcisio Pequeno
Série “O que nos faz pensar”,
Cadernos do Departamento de Filosofia da PUC-Rio, v. 3, pgs. 81-96, 1990.
Resumo: Uma definição do método
dos tableaux de um modo independente das lógicas consideradas, incluindo
exemplos para a lógica quantificacional clássica e para a
lógica paracompleta P1 de Newton C. A. da Costa,
juntamente com algumas heurísticas para a construção
de sistemas de tableaux.
Download (95 Kbytes)